/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#3=STAN2/FONT#4=NGB25/FONT#9=NGR20

␈↓ ↓H␈↓βS␈↓∧Computer Science Department, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4330 ␈↓ 
↓29 August 1980




␈↓ ↓H␈↓Director, Defense Advanced Research Projects Agency
␈↓ ↓H␈↓Department of Defense
␈↓ ↓H␈↓Washington, D. C.

␈↓ ↓H␈↓␈↓αSubject:␈↓ αH␈↓Quarterly Management Report
␈↓ ↓H␈↓␈↓ 	j␈↓	Form approved, Budget
␈↓ ↓H␈↓	␈↓ 	oBureau No. 22-RO293.␈↓

␈↓ ↓H␈↓␈↓αARPA Order Number:␈↓ 2494␈↓ εX␈↓αContract Number:␈↓ MDA903-80-C-0102

␈↓ ↓H␈↓␈↓αProgram Code Number:␈↓ 2D338␈↓ εX␈↓αPrincipal Investigator:␈↓ Prof. John McCarthy
␈↓ ↓H␈↓␈↓ ↓x␈↓ εX␈↓ π_415 497-4430

␈↓ ↓H␈↓␈↓αName of Contractor:␈↓  Board of Trustees of the Leland Stanford Junior University

␈↓ ↓H␈↓␈↓αE≥ective Date of Contract:␈↓ 1 October 1979␈↓ εX␈↓αShort Title of Work:␈↓ Computer Science
␈↓ ↓H␈↓␈↓ ↓x␈↓ εX␈↓ π_Research
␈↓ ↓H␈↓␈↓αContract Expiration Date:␈↓ 30 September 1981

␈↓ ↓H␈↓␈↓αAmount of Contract:␈↓  $817,872


␈↓ ↓H␈↓Dear Sir:

␈↓ ↓H␈↓Recent␈αexternal␈αpublications␈αof␈αour␈αsta≥␈αhave␈αbeen␈αon␈αformal␈αreasoning␈α[Reference␈α11],␈αprogram
␈↓ ↓H␈↓veri≡cation␈α[14,␈α15],␈αand␈αadvanced␈αcomputer␈αarchitectures␈α[12,␈α13].␈α Members␈αof␈αour␈αsta≥␈αrecently
␈↓ ↓H␈↓published␈α∞Ph.D.␈α∞dissertations␈α∞on␈α∞formal␈α∞reasoning␈α∞[1,␈α∞8],␈α∞knowledge-based␈α∞reasoning␈α∞[3,␈α∞5],␈α
and
␈↓ ↓H␈↓robotics␈α∪[9].␈α∀ Other␈α∪reports␈α∀appeared␈α∪on␈α∀mathematical␈α∪theory␈α∀of␈α∪computation␈α∀[2],␈α∪computer
␈↓ ↓H␈↓graphics [4], formal reasoning [6], and a text editor [7].

␈↓ ↓H␈↓α␈↓ ¬Research Program and Plan 

␈↓ ↓H␈↓No change.

␈↓ ↓H␈↓α␈↓ ¬#Major Accomplishments 

␈↓ ↓H␈↓None.

␈↓ ↓H␈↓α␈↓ ¬1Problems Encountered 

␈↓ ↓H␈↓Nothing new.
␈↓ ↓H␈↓␈↓αDirector, DARPA␈↓ ¬d29 August 1980␈↓ 
nPage 2


␈↓ ↓H␈↓α␈↓ ¬rFiscal Status 

␈↓ ↓H␈↓Amount currently funded:␈↓ 
Z$305,000 

␈↓ ↓H␈↓Estimated expenditures and commitments (through 30 June 1980): ␈↓ 
Z$189,656 

␈↓ ↓H␈↓Estimated funds required to complete the work (through 30 September 1981): ␈↓ 
Z$817,872 

␈↓ ↓H␈↓α␈↓ ∧SAction Required by the Government 

␈↓ ↓H␈↓None.

␈↓ ↓H␈↓α␈↓ ¬rFuture Plans 

␈↓ ↓H␈↓No change.

␈↓ ↓H␈↓␈↓ πhBest regards,



␈↓ ↓H␈↓␈↓ πhJohn McCarthy
␈↓ ↓H␈↓␈↓ πhProfessor of Computer Science



␈↓ ↓H␈↓cc: addressee - 2 copies, John McCarthy, Robert Kahn (ARPA), ONR Stanford.


␈↓ ↓H␈↓α␈↓ ¬cREFERENCES 

␈↓ ↓H␈↓1.  David E.  Wilkins, ␈↓αUsing Patterns and Plans to Solve Problems and Control Search␈↓, Thesis:
␈↓ ↓H␈↓␈↓ ↓xPhD in Computer Science, Stanford A. I. Memo AIM-329, June 1979.

␈↓ ↓H␈↓2.  Zohar Manna and Amir Pnueli, ␈↓αThe Modal Logic of Programs␈↓, Stanford A. I. Memo
␈↓ ↓H␈↓␈↓ ↓xAIM-330, September 1979.

␈↓ ↓H␈↓3.  Elaine Kant, ␈↓αE≠ciency Considerations in Program Synthesis: A Knowledge-Based
␈↓ ↓H␈↓α␈↓ ↓xApproach␈↓, Thesis: PhD in Computer Science, Stanford A. I. Memo AIM-331, July 1979.

␈↓ ↓H␈↓4.  Donald E. Knuth, ␈↓αMETAFONT, a system for alphabet design␈↓, Stanford A. I. Memo
␈↓ ↓H␈↓␈↓ ↓xAIM-332, September 1979.

␈↓ ↓H␈↓5.  Brian McCune, ␈↓αBuilding Program Models Incrementally from Informal Descriptions␈↓,
␈↓ ↓H␈↓␈↓ ↓xThesis: PhD in Computer Science, Stanford A. I. Memo AIM-333, October 1979.

␈↓ ↓H␈↓6.  John McCarthy, ␈↓αCircumscription - A Form of Non-Monotonic Reasoning␈↓, Stanford A. I.
␈↓ ↓H␈↓␈↓ ↓xMemo AIM-334, February 1980.
␈↓ ↓H␈↓␈↓αDirector, DARPA␈↓ ¬d29 August 1980␈↓ 
nPage 3


␈↓ ↓H␈↓7.  Arthur Samuel, ␈↓αEssential E␈↓, Stanford A. I. Memo AIM-335, March 1980.

␈↓ ↓H␈↓8.  Martin Brooks, ␈↓αDetermining Correctness by Testing␈↓, Thesis: PhD in Computer Science,
␈↓ ↓H␈↓␈↓ ↓xStanford A. I. Memo AIM-336, May 1980.

␈↓ ↓H␈↓9.  Morgan Ohwovoriole, ␈↓αAn Extention of Screw Theory and its Application to the
␈↓ ↓H␈↓α␈↓ ↓xAutomation of Industrial Assemblies␈↓, Thesis: PhD in Mechanical Engineering, Stanford A.
␈↓ ↓H␈↓␈↓ ↓xI. Memo AIM-338, April 1980.

␈↓ ↓H␈↓10.  Aiello, Luigia and G. Prini, ␈↓αDesign of a personal computing system␈↓, ␈↓↓Proc. Annual Conf. of
␈↓ ↓H␈↓↓␈↓ ↓xthe Canadian Information Processing Society␈↓, Victoria (British Columbia), May 12-14, 1980.

␈↓ ↓H␈↓11.  Goad, Chris, ␈↓αProofs as descriptions of computations␈↓, ␈↓↓Proc. Automatic Deduction Conference␈↓,
␈↓ ↓H␈↓␈↓ ↓xLes Arcs (France), July 8-11, 1980.

␈↓ ↓H␈↓12.  Moravec, Hans P., ␈↓αFully Interconnecting Multiple Computers with Pipelined Sorting Nets␈↓,
␈↓ ↓H␈↓␈↓ ↓x␈↓↓IEEE Trans. on Computers␈↓, October 1979.

␈↓ ↓H␈↓13.  Moravec, Hans, ␈↓αThe Endless Frontier and The Thinking Machine␈↓, ␈↓↓The Endless Frontier␈↓,
␈↓ ↓H␈↓␈↓ ↓xVol. 2, Jerry Pournelle, ed., Grosset & Dunlap, Ace books, 1980. (to appear)

␈↓ ↓H␈↓14.  Nelson, C.G. and Oppen, D., ␈↓αSimpli≡cation by Cooperating Decision Procedures␈↓, ␈↓↓ACM
␈↓ ↓H␈↓↓␈↓ ↓xTransactions on Programming Languages and Systems␈↓, Oct. 1979.

␈↓ ↓H␈↓15.  Polak, Wolfgang, ␈↓αAn exercise in automatic program veri≡cation␈↓, ␈↓↓IEEE Trans. on Software
␈↓ ↓H␈↓↓␈↓ ↓xEngineering␈↓, vol. SE-5, Sept. 1979.